(@$i$ $M$)($j$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$if eqof(IdDeq)($j$,$i$)$\rightarrow$ $M$ else  fi